Casper CBC: Formal verification
Runtime Verification
Elaine Li, Traian S,erb ̆anut, ̆a, Denisa Diaconescu, Grigore Rosu, VladZamfir
Target
Minimal framework
Safety
Non-triviality
Light client
Define validators as "Comparable" type
https://gyazo.com/7f3ec5373541145bc423befb66cf662c
StrictlyComparable contains:
a proof that there exists at least one witness of type X (inhabited)
a comparison operator which takes two elements of type X and returns either Lt, Eq or Gt (compare)
and a proof that this comparison operator imposes a strict ordering on elements of type X (compare_strictorder)
Abstract away messages from states, state transitions, fault weights
State
https://gyazo.com/e604bb9bca200f746130da5668685e24
Reachability of states
https://gyazo.com/dadc4088747465c2f14ff9f0845d9030
Fault weight
https://gyazo.com/755d4c0155de8a5e6e6c9a9db7ea55a9
nrryuya.icon > The decoupled "mutually recursive definition of states and messages" are only handled in the definition of full node and not in the safety and non-triviality proofs
Strong non-triviality
Non-triviality = the existence of a protocol property$ Pfor which there is a protocol state$ \sigma_1that is decided on$ Pand another protocol state$ \sigma_2that is decided on$ ¬P
"In our generalization efforts, we found that non-triviality precisely captures the notion of non-local confluence in the abstract rewriting system literature"
Strong non-triviality = for every protocol state s1, there exists a protocol state s2 that is s1’s next state and a protocol state s3 that is s1’s future state, such that s1 and s3 share a common future, but s2 and s3 do not
Proved by full/light node specification but not only by abstract definition
LayerX
Isabelle/HOL
Target
Minimal framework
Safety
State transition
(WIP) LMD GHOST
Simple finality detector
Previous work
CBC Casper binary consensus in Isabelle/HOL (2017 Mar) by pirapira
Trail of Bits
PlusCal and TLA+
Liveness without message delay